ap2(f, x) -> x
ap2(ap2(ap2(g, x), y), ap2(s, z)) -> ap2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
↳ QTRS
↳ Non-Overlap Check
ap2(f, x) -> x
ap2(ap2(ap2(g, x), y), ap2(s, z)) -> ap2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
ap2(f, x) -> x
ap2(ap2(ap2(g, x), y), ap2(s, z)) -> ap2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
ap2(f, x0)
ap2(ap2(ap2(g, x0), x1), ap2(s, x2))
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(x, y)
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(x, y), 0)
ap2(f, x) -> x
ap2(ap2(ap2(g, x), y), ap2(s, z)) -> ap2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
ap2(f, x0)
ap2(ap2(ap2(g, x0), x1), ap2(s, x2))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(x, y)
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(x, y), 0)
ap2(f, x) -> x
ap2(ap2(ap2(g, x), y), ap2(s, z)) -> ap2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
ap2(f, x0)
ap2(ap2(ap2(g, x0), x1), ap2(s, x2))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(x, y)
ap2(f, x) -> x
ap2(ap2(ap2(g, x), y), ap2(s, z)) -> ap2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
ap2(f, x0)
ap2(ap2(ap2(g, x0), x1), ap2(s, x2))
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(x, y)
Used ordering: Combined order from the following AFS and order.
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
AP1 > ap2
[g, s, 0]
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
ap2(f, x) -> x
ap2(ap2(ap2(g, x), y), ap2(s, z)) -> ap2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
ap2(f, x0)
ap2(ap2(ap2(g, x0), x1), ap2(s, x2))